(*
 * Copyright (c) 2009, Palle Raabjerg
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 *   * Redistributions of source code must retain the above copyright notice,
 *     this list of conditions and the following disclaimer.
 *   * Redistributions in binary form must reproduce the above copyright notice,
 *     this list of conditions and the following disclaimer in the documentation
 *     and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE
 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
 * POSSIBILITY OF SUCH DAMAGE.
 *)

(** Generate constraints from messages and processes *)

open Constraints;;

module SMap = Map.Make(String);;

(** Class for generating unique strings.
*)
class genstring prefix =
object
  val mutable counter = 0
  method fresh =
    let countval = counter in
      counter <- counter + 1;
      prefix ^ (string_of_int countval)
end;;

let typevar = new genstring "T";;
let effectvar = new genstring "R";;
let namegen = new genstring "x";;

(** Object for collecting messages for postprocessing *)
let messages =
object
  val mutable msglist = []
  method add msg =
    msglist <- msg::msglist
  method get =
    msglist
end;;

(** Object for collecting environments for postprocessing *)
let environments =
object
  val mutable envlist = []
  method add env =
    envlist <- env::envlist
  method get =
    envlist
end;;


exception NoName of string;;

(** Find the type of a name in an environment
    @param x Name
    @param env Environment

    @return Type of x in env
*)
let rec nametype x env =
  match env with
    | [] -> raise (NoName ("Name " ^ x ^ " not found in environment"))
    | Type(name, typvar)::restenv ->
	if x = name then
	  Type(name, typvar)
	else
	  nametype x restenv
    | UnType(name)::restenv ->
	if x = name then
	  UnType(name)
	else
	  nametype x restenv
    | Effect(_)::restenv ->
	nametype x restenv
(*    | EffectVar(_)::restenv ->
	nametype x restenv*)
(*    | Empty::restenv ->
	nametype x restenv*)
;;

(** Extract environment from process
    @param proc Process

    @return Environment extracted from proc
*)
let rec env_of proc =
  match proc with
    | Spitree.PPara(p, q) -> List.append (env_of q) (env_of p)
    | Spitree.Nu(x, _, p) -> List.append (env_of p) [Type(x, typevar#fresh)]
    | Spitree.Begin(l, m) -> [Effect(Reso(l, m))]
    | _ -> [];;

let rec collect_list_mayeq formula =
  let from_typec typec =
    match typec with
      | MayEqual(tvar, basetype) -> [(tvar, basetype)]
      | _ -> []
  in
    match formula with
      | TypeC(tconstraint) -> from_typec tconstraint
      | (EffectC(_) | EnvC(_)) -> []
      | (And(f1, f2) | Or(f1, f2) | Leadsto(f1, f2)) -> List.append (collect_list_mayeq f1) (collect_list_mayeq f2)
      | Forall(_, f) -> collect_list_mayeq f
      | (Conjunction(flist) | CommentConjunction(_, flist)) ->
	  List.fold_left (fun coll_list f ->
			    List.append (collect_list_mayeq f) coll_list
			 ) [] flist
      | True -> []

let table_of_list_mayeq may_list =
  let may_table = Hashtbl.create 100 in
    List.iter (fun (tvar, basetype) ->
		 Hashtbl.add may_table tvar basetype
	      ) may_list;
    may_table

(*let propagate_abstraction formula =
  let may_table = table_of_list_mayeq (collect_list_mayeq formula) in
  let in_typec typec =
    
    match formula with
      | 
*)
exception Bug of string;;
exception TypeMismatch of string;;

(** Extract constraint formula from message, given environment
    @param env Environment
    @param msg Message

    @return Constraint formula
*)
let rec constraint_of_msg env msg =
  environments#add env;
  match msg with
    | Spitree.Encr(m, n) ->
	let (ut1, psi1) = constraint_of_msg env m in
	let (ut2, psi2) = constraint_of_msg env n in
	let ut3 = typevar#fresh in
	  (ut3,
	   CommentConjunction("(Msg Encr)",
	     [TypeC(Equal(ut3, Un));
	      TypeC(MayEqual(ut2, Key(ut1)));
	      Leadsto(TypeC(Equal(ut2, Un)),
		      TypeC(Equal(ut1, Un)));
	      psi1;
	      psi2
	     ]
	   ))
    | Spitree.MPair(m, n) ->
	let (ut1, psi1) = constraint_of_msg env m in
	let (ut2, psi2) = constraint_of_msg env n in
	let ut = typevar#fresh in
	let ut2p = typevar#fresh in
	let x = namegen#fresh in
	  (ut,
	   CommentConjunction("(Msg Pair)",
	     [TypeC(MayEqual(ut, Pair(x, ut1, ut2p)));
	      TypeC(MayEqual(ut2p,Abstraction(ut2, m, x)));
	      Leadsto(And(TypeC(Equal(ut1,Un)),TypeC(Equal(ut2,Un))),
		      TypeC(Equal(ut,Un)));
	      psi1;
	      psi2
	     ]
	   ))
    | Spitree.Name(x) ->
	let xtype = nametype x env in
	  (match xtype with
	    | Type(_, tv) ->
		(tv,
		 CommentConjunction("(Msg Name)",
		   [TypeC(HasType(x,tv));
		    EnvC(WellFormed(env))]
		 ))
	    | UnType(_) ->
		let ut = typevar#fresh in
		  (ut,
		   CommentConjunction("(Msg Name Un)",
		     [TypeC(HasType(x,ut));
		      TypeC(Equal(ut,Un));
		      EnvC(WellFormed(env))]
		   ))
	    | _ -> raise (Bug ("Received effect or empty from the nametype function. This should never happen. nametype is not constructed that way."))
	  )
    | Spitree.Ok ->
	let r = effectvar#fresh in
	let ut = typevar#fresh in
	  (ut,
	   CommentConjunction("Msg Ok",
	     [TypeC(HasType("ok", ut));
	      Leadsto(TypeC(Equal(ut,Un)),
		      EnvC(WellFormed(env)));
	      TypeC(MayEqual(ut,Ok(r)));
	      Leadsto(TypeC(NotUn(ut)),
		      And(EffectC(Instantiates(env, r)), EnvC(WellFormed(env))))]
	   ))
;;

(** Extract constraint formula from process, given environment
    @param env Environment
    @param proc Process

    @return Constraint formula
*)
let rec constraint_of_proc env proc =
  environments#add env;
  match proc with
    | Spitree.Out(m, n) ->
	let (ut1, psi1) = constraint_of_msg env m in
	let (ut2, psi2) = constraint_of_msg env n in
	  messages#add m; messages#add n;
	  CommentConjunction("(Proc Out)",
	    [TypeC(MayEqual(ut1,Ch(ut2)));
	     Leadsto(TypeC(Equal(ut1, Un)),
		     TypeC(Equal(ut2, Un)));
	     psi1;
	     psi2]
	  )
    | (Spitree.In(m, x, p)|Spitree.InRepl(m, x, p)) ->
	let (ut1, psi1) = constraint_of_msg env m in
	let ut2 = typevar#fresh in
	let psi2 = constraint_of_proc (Type(x, ut2)::env) p in
	  messages#add m;
	  CommentConjunction("(Proc In)",
	    [TypeC(MayEqual(ut1,Ch(ut2)));
	     Leadsto(TypeC(Equal(ut1, Un)),
		     TypeC(Equal(ut2, Un)));
	     psi1;
	     psi2]
	  )
    | Spitree.Nu(x, _, p) ->
	let ut = typevar#fresh in
	let psi1 = constraint_of_proc (Type(x, ut)::env) p in
	  CommentConjunction("(Proc Res)",
			     [EnvC(NotInDom(x, env));
			      psi1;
			      Leadsto(TypeC(NotGenerative(ut)), TypeC(Fail))
			     ]
			    )
    | Spitree.PPara(p, q) ->
	let psi1 = constraint_of_proc (List.append (env_of q) env) p in
	let psi2 = constraint_of_proc (List.append (env_of p) env) q in
	  CommentConjunction("(Proc Par)",
			    [psi1; psi2])
    | Spitree.PNil ->
	True
    | Spitree.Begin(l, m) ->
	messages#add m;
	CommentConjunction("(Proc Begin)",
			   [EnvC(NamesInDom(m,env));
			    EnvC(WellFormed(env))])
    | Spitree.End(l, m) ->
	messages#add m;
	CommentConjunction("(Proc End)",
			   [EffectC(EffectIncl(l,m,env));
			    EnvC(WellFormed(env))])
    | Spitree.Decrypt(m, y, _, n, p) ->
	let (ut1, psi1) = constraint_of_msg env m in
	let (ut2, psi2) = constraint_of_msg env n in
	let ut3 = typevar#fresh in
	let psi3 = constraint_of_proc (Type(y, ut3)::env) p in
	  messages#add m; messages#add n;
	  CommentConjunction("(Proc Decrypt)",
	    [TypeC(Equal(ut1,Un));
	     TypeC(MayEqual(ut2,Key(ut3)));
	     Leadsto(TypeC(Equal(ut2,Un)),
		     TypeC(Equal(ut3,Un)));
	     psi1;
	     psi2;
	     psi3
	    ]
	  )
    | Spitree.Split(m, x, _, y, _, p) ->
	let (ut0, psi1) = constraint_of_msg env m in
	let ut1, ut2 = typevar#fresh, typevar#fresh in
	let psi2 = constraint_of_proc (Type(y, ut2)::Type(x, ut1)::env) p in
	  messages#add m;
	  CommentConjunction("(Proc Split)",
	    [TypeC(MayEqual(ut0,Pair(x, ut1, ut2)));
	     Leadsto(TypeC(Equal(ut0,Un)),
		     And(TypeC(Equal(ut1,Un)), TypeC(Equal(ut2,Un))));
	     psi1;
	     psi2
	    ]
	  )
    | Spitree.Match(m, _, n, y, _, p) ->
	let (ut1, psi1) = constraint_of_msg env m in
	let (ut2, psi2) = constraint_of_msg env n in
	let ut0, ut3, ut4 = typevar#fresh, typevar#fresh, typevar#fresh in
	let psi3 = constraint_of_proc (Type(y, ut3)::env) p in
	let x = namegen#fresh in
	  messages#add m; messages#add n;
	  CommentConjunction("(Proc Match)",
	    [TypeC(MayEqual(ut1,Pair(x, ut0, ut4)));
	     TypeC(MayEqual(ut3,Application(ut4,n)));
	     Leadsto(TypeC(Equal(ut1, Un)),
		     Conjunction([TypeC(Equal(ut2, Un));
				  TypeC(Equal(ut0, Un));
				  TypeC(Equal(ut3, Un));
				  TypeC(Equal(ut4, Un))
				 ])
		    );
	     psi1;
	     psi2;
	     psi3
	    ]
	  )
;;
